Faster Algorithms for Weighted Recursive State Machines

摘要

Pushdown systems (PDSs) and recursive state machines (RSMs), which arelinearly equivalent, are standard models for interprocedural analysis. Yet RSMsare more convenient as they (a) explicitly model function calls and returns,and (b) specify many natural parameters for algorithmic analysis, e.g., thenumber of entries and exits. We consider a general framework where RSMtransitions are labeled from a semiring and path properties are algebraic withsemiring operations, which can model, e.g., interprocedural reachability anddataflow analysis problems. Our main contributions are new algorithms for several fundamental problems.As compared to a direct translation of RSMs to PDSs and the best-known existingbounds of PDSs, our analysis algorithm improves the complexity forfinite-height semirings (that subsumes reachability and standard dataflowproperties). We further consider the problem of extracting distance values fromthe representation structures computed by our algorithm, and give efficientalgorithms that distinguish the complexity of a one-time preprocessing from thecomplexity of each individual query. Another advantage of our algorithm is thatour improvements carry over to the concurrent setting, where we improve thebest-known complexity for the context-bounded analysis of concurrent RSMs.Finally, we provide a prototype implementation that gives a significantspeed-up on several benchmarks from the SLAM/SDV project.